$\forall$${\it ds}$:$x$:Id fp$\rightarrow$ Type$_{\mbox{\scriptsize i}}$. normal{-}ds\{i:l\}(${\it ds}$) $\in$ Prop$_{\mbox{\scriptsize i'}}$